
\section{Introduction}

Backbones are firstly generalized from the coloring problem. A pair of nodes are backbones if they always have the same color in every possible k-coloring\cite{WTS2001}.

In satisfiability problem, given a formulae $\Phi$, an truth assignment is a map from boolean variables to literals appeared in $\Phi$. In an assignment, a literal can only be assigned as TRUE or FALSE. Given an assignment $\lambda$, if there exist at least one literal in a clause $\phi\in\Phi$ that has been assigned as TRUE according to $\lambda$, $\phi$ is called to be satisfied by $\lambda$. If there exists a $\lambda$ that satisfy every clause $\phi\in\Phi$, $\lambda$ is a model or a satisfied assignment of $\Phi$.
Backbones of a propositional formula $\Phi$ is a cluster of literals that are TRUE in every model of $\Phi$\cite{BCJ2001,KPJ2005}.

Backbones have been studied in random 3-SAT problems \cite{DOG2001}, optimization problems\cite{CJG2001,KPS2005,WTS2001}, as well as Maximal Satisfiability(MSS) problems\cite{MM2005}.
As shown in \cite{ZWR2003}, backbones are applied to local minima of Walksat and improves the performance of Walksat by making biased moves in a local search. Another similar application of backbones information is shown in \cite{ZWL2005}, in this experiment, backbones information significantly contributes to the acceleration of Lin-Kernighan(LK) local search family algorithms when dealing with Travel Salesman Problem(TSP).
A more recent application of backbones arises in \cite{Z11}. A number of backbones extracting approaches are proposed and applied to post silicon fault localisation. The results show that backbones extracting using SAT solvers are suitable for large scale applications with only a little SAT solver calls.

As shown above, finding backbones is the key in many practical applications, such as planning problem and constraint satisfaction problem. It has been proved that backbones computing is a co-NP problem\cite{Jan10}, which have rise huge challenges.
A number of backbones extraction algorithms have been proposed in recent years. All state-of-the-art backbones extraction approaches employ SAT solvers, MiniSAT\cite{MINISAT} for most of them.
Implicant enumeration\cite{MK2002,RSF2004} enumerates implicants of formula $\Phi$ one by one and updates the backbones estimation in each iteration. The negation of an implicant is added to $\Phi$ in order to avoid finding the same implicant. For an implicant $\lambda$, the negation of $\lambda$ is $\bigvee_{l\in\lambda}\neg l$. Standard implicants reducing techniques can be applied to mitigate the size of blocking clauses. It have to enumerate all models of $\Phi$ before the algorithm terminates, which is unnecessary costly.

Zhu et al, proposed an iterative SAT testing algorithm \cite{Z11}. The algorithm maintains an estimation of backbones $\Phi_\BL$. The negation of $\Phi_\BL$ is the disjunction of each complementing literals in backbones estimation, i.e., $\neg\Phi_\BL=\bigvee_{\neg l}, l\in\Phi_\BL$. In each iteration, a clause that formed by $\neg \Phi_\BL$ conjuncted to $\Phi$ and formed $\Phi'$. If $\Phi'$ is satisfiable, it means that at least one non-backbone is in the backbone estimation, estimation is refined by removing the non-backbone literal. The process is repeated until $\Phi'$ is not satisfiable any longer. Along with the estimation, the clauses number of $\Phi'$  is monotone increasing due to the continuously disjunction in each iteration, which dramatically promote the complexity of $\Phi'$. In other words, for each iteration, it takes longer CPU time than the last iteration.

The Core Based Algorithm presented in \cite{JLM15} is stable and effectiveness. It considers complementing of the model as assumptions input for SAT solver in each iteration. If $\Phi$ is unsatisfied under given assumptions, a core is returned by SAT solver to indicate reasons. According to the implementation of MiniSAT 2.2 \cite{MINISAT}, the reason is a part of the given assumptions. Whenever there is exactly one literal in the reason, the literal is a backbone. If there is more than one literal in the reason, they will be marked as visited. If every literal in an iteration is visited, iterative SAT testing will be invoked to test the rest of unmarked literals. According to the author, for the lower percentages of backbones, Core Based Algorithms are significantly better. When the percentage of backbone is over 25\%, Core Based Algorithm behave very similarly Iterative SAT Testing Algorithm.

Revisited previous researches, backbones computing of low density backbones formulae is quiet efficiencies and efficiency. In this paper, we focus on the hard instance, proposed a novel approach to spot non-backbones ahead and to estimate backbones. Instead of accumulating clauses to formula like Iterative SAT testing does, we test the literals one by one by leveraging assumptions. Assumptions are a group of literals. We consider assumptions as a kind of constraint input, it means that the literals in assumptions must be assigned to true in an assignment. If there exists a model $\lambda$ such that it satisfy every literals in assumptions, the formula is satisfied under these assumptions. According to the satisfiability theory, assumptions are equivalence to clauses that only contains the assumption literal. Compared with clauses conjunction, assumptions won't increase the complexity of formula since no clauses are added to the formula. Also, assumptions is more suitable for iterative SAT testing since it can be reset in each iteration.

Using variables clauses coverage analysis, a group of non-backbone literals and an estimation of backbones are obtained, refereed as $\NBL_u$ and $\HDBS$, respectively. For each literals in $\HDBS$, Minisat with assumptions will be evoked. The only assumption in each iteration is the current testing literal. If Minisat returns false, the literal is a backbone, it will be conjuncted with the original formula to simplify it.

The approach leveraging Whitening Algorithm and other pervious backbones computing algorithms, designed and implemented a Multi Estimation Based Algorithms (MEB) , experiments are conducted to evaluate MEB, results showed that MEB is compatible with Core Based Algorithm when dealing with low density backbones formulae. For hard formulae with dense backbones, MEB outperforms Core Based Approach considering the total SAT solver time and SAT calls number.
Compared with Core Based Algorithm which directly calculate backbones. MEB estimate non-backbone literals and backbone literals ahead.
Unlike the Iterative SAT Testing approach, the estimation doesn't need to rely on SAT solvers. Only one SAT solver call is needed during the estimation process. 
%FCB will first compute the under-approximation of non-backbone literals, referred as $\NBL_u$ in $O(n^2)$ time. With the $\NBL_u$ information, a group of literals with dense backbones will be estimated in polynomial time, refereed as $\HDBS$.
%Iterative SAT testing per literals of $\HDBS$ will be applied to determine whether a literal is a backbone or not. A backbone literal will be conjuncted with formula as a new unit clause. With several backbones, formula will be simplified\cite{MPA2015}.
Experiments indicate that, the average dense of backbones in $\HDBS$ is over 50\%, which helps MEB to recognize more backbones in less SAT solver calls than CB needs. Especially for hard formulae, MEB will save a large amount of CPU time since it invoking less Minisat than CB does.

This paper is organized as follows.
Section 2 introduces the concept of backbones.
Section 3 relates backbones estimate reducing procedures to Core Based Backbones Extraction Algorithms and evolved to Filter Core Based(FCB) Backbone Extraction Algorithms.
Section 4 presents the experimental evaluation of FCB.
Section 5 makes a conclusion and discusses about future work.
